1. Field of the Invention
This invention relates generally to the formal verification of a logic design, and more particularly, to the formal verification of temporal properties defined using local variables.
2. Description of the Related Art
SystemVerilog is a hardware design and verification language. SystemVerilog Assertions (SVA) is a subclass of SystemVerilog, used to declaratively specify functional behaviors of hardware designs. Similarly, Property Specification Language (PSL) is used to declaratively specify functional behaviors of hardware designs independent of the design language. Typically, SVA and PSL properties are validated during dynamic simulation or are formally verified.
SystemVerilog Assertions (SVA), as well as Property Specification Language (PSL) are linear temporal logics, extended with regular expressions and local variables. Moreover, it is known that the complexity of the verification problem for PSA or SVA is PSPACE-complete in the absence of (a) time windows, (b) intersection and (c) local variables. In addition, the verification problem for PSA or SVA with any one of these three renders the problem to the higher complexity class EXPSPACE. Furthermore, local variables create a complexity hurdle more easily. An upper bound is achieved by constructing an alternating Büchi automaton of size proportional to the size of the property and the size of the Cartesian product of the domains of the local variables. Seeing local variables of large domain is very common, for instance, when asserting data consistency on bus protocols. Thus, a 64-bit bus results in a single variable domain of size 264. Building an alternating automaton of more than 264 states may be possible, but for model checking it is translated into a non-deterministic Büchi automaton of more than 2^(264) states, represented by 264 state variables, which is infeasible.
The addition of local variables renders the verification problem of SVA and PSL formulae EXPSPACE-complete and therefore unpractical. Thus, there is a need for a practical method for formally verifying SVA and PSL formulae defined using local variables.